Section: Application Domains

Certified decision procedures

Roughly in the last ten years, proof systems have enjoyed a wider and wider audience, having been used by a growing number of researchers and teams for a growing number of applications. We can list a dozen of INRIA teams who have used Coq in an important way. We can also list the various application fields. It comes as no surprise that these fields are often parts of the genuine activities of other related INRIA teams and appear in more detail in their own reports; among others:

• Computer security: from the formalization of security properties of protocols, to the analysis of cryptographic primitives, through questions of privacy.

• Embedded software, with a growing emphasis on real-time, reactive, software.

• Computer arithmetic: certifying the correctness of the implementation of numerical functions, possibly with explicit rounding errors.

• Formally certified automatic demonstration techniques (like SAT/SMT solvers) either for more trustworthy automatic tools, or to use the latter as formal proof techniques.